@$i$[[$x$;${\it snd}$;${\it upd}$]]
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$l$$\in$msg{-}spec{-}links(${\it snd}$).@$i$[[$x$;${\it snd}$]] \& $\forall$$z$$\in$update{-}spec{-}vars(${\it upd}$).@$i$[[$x$;${\it upd}$]]